package tr.edu.ege.kipler.satisfiability.container.operational;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.clash.ClashDetectionStrategy;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.FormulaBase;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class ClashDetectionObserver implements ABoxChangeObserver {
	private ClashDetectionStrategy clashStrategy;

	public ClashDetectionObserver(ClashDetectionStrategy clashStrategy) {
		setClashStrategy(clashStrategy);
	}

	public ClashDetectionStrategy getClashStrategy() {
		return clashStrategy;
	}

	public void setClashStrategy(ClashDetectionStrategy clashStrategy) {
		this.clashStrategy = clashStrategy;
	}

	public void afterFormulaIsAdded(FormulaBase fBase, Formula formula)
			throws UnsatisfiableException {
		ABox abox = (ABox) fBase;
		if (getClashStrategy().hasClash(abox, formula)) {
			abox.setHasClash(true);
			throw new UnsatisfiableException(clashStrategy.getDependencySet(),
					clashStrategy.getExplanation());
		}
	}

	public void afterNodeIsRemoved(FormulaBase fBase, Individual indv) {
		// Nothing to do
	}
}
